r:Rng, a, b:|r|. ((-r(a)) * b) = -r(a * b)  |r| & (a * (-r(b))) = -r(a * b)  |r| 

latex

Up	rings 1
Definitions of Statement	Rng
Definitions	t  T, P & Q, x:A. B(x), x f y, P  Q, P  Q, P  Q, Rng
Lemmas	rng wf, rng car wf, rng minus wf, rng times wf, rng plus cancel l, rng plus inv, rng plus wf, rng zero wf, rng times over plus, rng times zero